R:Realizer.
(R-size(R)  1)
 (R-discrete(R)
 (~
 (if Reffect?(R) Rinit?(R)
 (then <R-loc(R), if Reffect?(R) then Reffect-x(R) else Rinit-x(R) fi > : case if Reffect?(R)
 (then <R-loc(R), if Reffect?(R) then Reffect-x(R) else Rinit-x(R) fi > : case then Reffect-f(R)
 (then <R-loc(R), if Reffect?(R) then Reffect-x(R) else Rinit-x(R) fi > : case else Rinit-v(R)
 (then <R-loc(R), if Reffect?(R) then Reffect-x(R) else Rinit-x(R) fi > : case fi 
 (then of inl(a) => tt
 (then o| inr(a) => ff
 (else 
 (fi ) 

latex

Definitions

x. t(x), t  T, ff, tt, Rinit-v(x1), Reffect-f(x1), Rinit-x(x1), Reffect-x(x1), R-loc(R), Rinit?(x1), Reffect?(x1), p q, if b then t else f fi , R-discrete(R), R-size(R), P  Q, x:A. B(x), , x(s), Unit, Realizer, Rrframe(loc;x;L), Rbframe(loc;k;L), Raframe(loc;k;L), Rpre(loc;ds;a;p;P), Rsends(ds;knd;T;l;dt;g), Reffect(loc;ds;knd;T;x;f), Rsframe(lnk;tag;L), Rframe(loc;T;x;L), Rinit(loc;T;x;v), left  right, , Rnone(),

Lemmas

es realizer wf, nat plus wf, R-size wf, le wf, bool wf, finite-prob-space wf, decl-type wf, decl-state wf, fpf wf, IdLnk wf, Knd wf, rationals wf, Id wf, unit wf